Given a universe , a -large set is a set which is not a -small set. -large sets can be contrasted with -small sets.
Every proper class in set theory is a -large set. However, in dependent type theory, only material proper classes are always -large h-sets; structural proper classes in dependent type theory are h-groupoids if the universe is a univalent universe.
Last revised on November 19, 2022 at 11:03:33. See the history of this page for a list of all contributions to it.